$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type).
\\[0ex]($\forall$$x$:IdLnk, $x_{1}$:Id. AtomFree(Type;$M$($x$,$x_{1}$)))
\\[0ex]$\Rightarrow$ ($\forall$$l$:IdLnk, ${\it tg}$:Id, $v$:$M$($l$,${\it tg}$). AtomFree($M$($l$,${\it tg}$);$v$))
\\[0ex]$\Rightarrow$ ($\forall$$m$:Msg($M$). AtomFree(Msg($M$);$m$))